section ‹Preliminaries›


theory Preliminaries imports "HOL-Cardinals.Cardinals"
begin

text ‹This section discusses preliminaries on families of items (technically,
partial functions from a type of {\em indexes})
that we call {\em inputs} because they will be inputs to the binding operations.
For inputs, we define some monad-like lifting operators.
We also define simple infinitely branching trees (with no info attached
to the nodes and with branching given by partial functions from
indexes) -- these will be used as ``skeletons'' for terms, giving a size 
on which we can induct.
›

abbreviation regular where "regular ≡ stable"
lemmas regular_UNION = stable_UNION


subsection ‹Trivia›


type_synonym 'a pair = "'a * 'a"

type_synonym 'a triple = "'a * 'a *'a"

type_synonym 'a rel = "'a pair set"


(* Selectors for triples *)

definition fst3 where "fst3 == fst"
definition snd3 where "snd3 == fst o snd"
definition trd3 where "trd3 == snd o snd"


lemma fst3_simp[simp]: "fst3 (a,b,c) = a"
unfolding fst3_def by simp


lemma snd3_simp[simp]: "snd3 (a,b,c) = b"
unfolding snd3_def by simp


lemma trd3_simp[simp]: "trd3 (a,b,c) = c"
unfolding trd3_def by simp


lemma fst3_snd3_trd3: "abc = (fst3 abc, snd3 abc, trd3 abc)"
unfolding fst3_def snd3_def trd3_def by auto


lemma fst3_snd3_trd3_rev[simp]:
"(fst3 abc, snd3 abc, trd3 abc) = abc"
using fst3_snd3_trd3[of abc] by simp


lemma map_id[simp]: "map id l = l"
unfolding id_def by simp


abbreviation max3 where
"max3 x y z == max (max x y) z"

lemmas map_id_cong = map_idI 
 
lemma ext2:
"(f ≠ g) = (∃ x. f x ≠ g x)"
using ext by auto

lemma not_equals_and_not_equals_not_in:
"(y ≠ x ∧ y ≠ x' ∧ phi) =
 (y ∉ {x,x'} ∧ phi)"
by simp


lemma mp2:
assumes "!! x y. phi x y ⟹ chi x y" and "phi x y"
shows "chi x y"
using assms by simp


lemma mp3:
assumes "!! x y z. phi x y z ⟹ chi x y z" and "phi x y z"
shows "chi x y z"
using assms by simp

lemma all_lt_Suc:
"(∀ i < Suc n. phi i) = ((∀ i < n. phi i) ∧ phi n)"
using less_Suc_eq by auto

declare hd_map[simp]
lemmas tl_map[simp] = list.map_sel 
declare last_map[simp] 

lemma tl_last[simp]:
assumes "tl L ≠ []"
shows "last (tl L) = last L"
using assms apply - by(induct L, auto)

lemma tl_last_hd:
assumes "L ≠ []" and "tl L = []"
shows "last L = hd L"
using assms apply - by(induct L, auto)



subsection ‹Lexicographic induction›

definition lt2 where
"lt2 == less_than <*lex*> less_than"

definition lt3 where
"lt3 == less_than <*lex*> lt2"

lemma wf_lt2:
"wf lt2"
unfolding lt2_def by auto

lemma wf_lt3:
"wf lt3"
unfolding lt3_def by (auto simp add: wf_lt2)

lemma lt2[intro]:
"!! k1 k2 j1 j2. k1 < j1 ⟹ ((k1,k2),(j1,j2)) ∈ lt2"
"!! k1 k2 j1 j2. ⟦k1 ≤ j1; k2 < j2⟧ ⟹ ((k1,k2),(j1,j2)) ∈ lt2"
unfolding lt2_def by auto

lemma lt3[intro]:
"!! k1 k2 k3 j1 j2 j3. k1 < j1 ⟹ ((k1,k2,k3),(j1,j2,j3)) ∈ lt3"
"!! k1 k2 k3 j1 j2 j3. ⟦k1 ≤ j1; k2 < j2⟧ ⟹ ((k1,k2,k3),(j1,j2,j3)) ∈ lt3"
"!! k1 k2 k3 j1 j2 j3. ⟦k1 ≤ j1; k2 ≤ j2; k3 < j3⟧ ⟹ ((k1,k2,k3),(j1,j2,j3)) ∈ lt3"
unfolding lt3_def by auto

lemma measure_lex2_induct:
fixes h1 :: "'a1 ⇒ nat" and h2 :: "'a2 ⇒ nat"
assumes
"!! x1 x2.
  ⟦(!! y1 y2. h1 y1 < h1 x1 ⟹ phi y1 y2);
   (!! y1 y2. ⟦h1 y1 ≤ h1 x1; h2 y2 < h2 x2⟧ ⟹ phi y1 y2)⟧
  ⟹ phi x1 x2"
shows "phi x1 x2"
proof-
  let ?chi = "%(n1,n2). ALL x1 x2. h1 x1 = n1 ∧ h2 x2 = n2 ⟶ phi x1 x2"
  {fix n1 n2
   have "?chi (n1,n2)"
   apply(rule wf_induct[of lt2 ?chi]) using wf_lt2 assms by blast+
  }
  thus ?thesis by blast
qed

lemma measure_lex3_induct:
fixes h1 :: "'a1 ⇒ nat" and h2 :: "'a2 ⇒ nat" and h3 :: "'a3 ⇒ nat"
assumes
"!! x1 x2 x3.
  ⟦(!! y1 y2 y3. h1 y1 < h1 x1 ⟹ phi y1 y2 y3);
   (!! y1 y2 y3. ⟦h1 y1 ≤ h1 x1; h2 y2 < h2 x2⟧ ⟹ phi y1 y2 y3);
   (!! y1 y2 y3. ⟦h1 y1 ≤ h1 x1; h2 y2 ≤ h2 x2; h3 y3 < h3 x3⟧ ⟹ phi y1 y2 y3)⟧
  ⟹ phi x1 x2 x3"
shows "phi x1 x2 x3"
proof-
  let ?chi = "%(n1,n2,n3). ALL x1 x2 x3. h1 x1 = n1 ∧ h2 x2 = n2 ∧ h3 x3 = n3 ⟶ phi x1 x2 x3"
  {fix n1 n2 n3
   have "?chi (n1,n2,n3)"
   apply(rule wf_induct[of lt3 ?chi]) using wf_lt3 assms by blast+
  }
  thus ?thesis by blast
qed


subsection ‹Inputs and lifting operators›

type_synonym ('index,'val)input = "'index ⇒ 'val option"

definition
lift :: "('val1 ⇒ 'val2) ⇒ ('index,'val1)input ⇒ ('index,'val2)input"
where
"lift h inp == λi. case inp i of None ⇒ None
                                |Some v ⇒ Some (h v)"

definition
liftAll :: "('val ⇒ bool) ⇒ ('index,'val)input ⇒ bool"
where
"liftAll phi inp == ∀ i v. inp i = Some v ⟶ phi v"

definition
lift2 ::
"('val1' ⇒ 'val1 ⇒ 'val2) ⇒ ('index,'val1')input ⇒ ('index,'val1)input ⇒ ('index,'val2)input"
where
"lift2 h inp' inp ==
 λi. case (inp' i, inp i) of
   (Some v',Some v) ⇒ Some (h v' v)
  |_ ⇒ None"

definition
sameDom ::  "('index,'val1)input ⇒ ('index,'val2)input ⇒ bool"
where "sameDom inp1 inp2 == ∀ i. (inp1 i = None) = (inp2 i = None)"


definition
liftAll2 :: "('val1 ⇒ 'val2 ⇒ bool) ⇒ ('index,'val1)input ⇒ ('index,'val2)input ⇒ bool"
where
"liftAll2 phi inp1 inp2 == (∀ i v1 v2. inp1 i = Some v1 ∧ inp2 i = Some v2 ⟶ phi v1 v2)"

lemma lift_None: "(lift h inp i = None) = (inp i = None)"
unfolding lift_def by (cases "inp i", auto)

lemma lift_Some:
"(∃ v. lift h inp i = Some v) = (∃ v'. inp i = Some v')"
using lift_None[of h inp i] by force

lemma lift_cong[fundef_cong]:
assumes "⋀ i v. inp i = Some v ⟹  h v = h' v"
shows "lift h inp = lift h' inp"
unfolding lift_def apply(rule ext)+
using assms by (case_tac "inp i", auto)

lemma lift_preserves_inj:
assumes "inj f"
shows "inj (lift f)"
unfolding inj_on_def apply auto proof(rule ext)
  fix inp inp' i assume *: "lift f inp = lift f inp'"
  show "inp i = inp' i"
  proof(cases "inp i")
    assume inp: "inp i = None"
    hence "lift f inp i = None" unfolding lift_def by simp
    hence "lift f inp' i = None" using * by simp
    hence "inp' i = None" by(auto simp add: lift_None)
    thus ?thesis using inp by simp
  next
    fix v assume inp: "inp i = Some v"
    hence "lift f inp i = Some (f v)" unfolding lift_def by simp
    hence "lift f inp' i = Some (f v)" using * by simp
    then obtain v' where inp': "inp' i = Some v'" and "f v' = f v"
    unfolding lift_def by(case_tac "inp' i", auto)
    hence "v = v'" using assms unfolding inj_on_def by simp
    thus ?thesis using inp inp' by simp
  qed
qed

lemma liftAll_cong[fundef_cong]:
assumes "⋀ i v. inp i = Some v ⟹ phi v = phi' v"
shows "liftAll phi inp = liftAll phi' inp"
unfolding liftAll_def apply((rule iff_allI)+) using assms by simp

lemma liftAll2_cong[fundef_cong]:
assumes "⋀ i v1 v2. ⟦inp1 i = Some v1; inp2 i = Some v2⟧ ⟹ phi v1 v2 = phi' v1 v2"
shows "liftAll2 phi inp1 inp2 = liftAll2 phi' inp1 inp2"
unfolding liftAll2_def apply((rule iff_allI)+) using assms by blast

lemma lift_ident: "lift (λv. v) inp = inp"
by(unfold lift_def, rule ext, case_tac "inp i", auto)

lemma lift_id[simp]:
"lift id inp = inp"
unfolding lift_def apply (rule ext) by(case_tac "inp i", auto)

lemma lift_comp: "lift g (lift f inp) = lift (g o f) inp"
by(unfold lift_def o_def, rule ext, case_tac "inp i", auto)

lemma liftAll_mono:
assumes "⋀ v. phi v ⟹ chi v" and "liftAll phi inp"
shows "liftAll chi inp"
using assms unfolding liftAll_def by blast

lemma liftAll_True: "liftAll (λv. True) inp"
unfolding liftAll_def by auto

lemma liftAll_lift_comp:  "liftAll phi (lift f inp) = liftAll (phi o f) inp"
unfolding liftAll_def o_def  
by (metis (mono_tags, lifting) lift_Some lift_def option.inject option.simps(5))

lemma liftAll_lift_ext:
"liftAll (λ x. f x = g x) inp = (lift f inp = lift g inp)"
unfolding lift_def liftAll_def 
by (auto simp: fun_eq_iff option.case_eq_if)  

lemma liftAll_and:
"liftAll (λ x. phi x ∧ chi x) inp = (liftAll phi inp ∧ liftAll chi inp)"
unfolding liftAll_def by blast

lemma liftAll_mp:
assumes "liftAll (λ v. phi v ⟶ chi v) inp" and "liftAll phi inp"
shows "liftAll chi inp"
using assms unfolding liftAll_def by auto

lemma sameDom_refl: "sameDom inp inp"
unfolding sameDom_def by auto

lemma sameDom_sym:
"sameDom inp inp' = sameDom inp' inp"
unfolding sameDom_def by auto

lemma sameDom_trans:
"⟦sameDom inp inp'; sameDom inp' inp''⟧ ⟹ sameDom inp inp''"
unfolding sameDom_def by auto

lemma sameDom_lift1:
"sameDom inp (lift f inp)"
unfolding sameDom_def lift_def 
by (auto simp: option.case_eq_if) 

lemma sameDom_lift2:
"sameDom (lift f inp) inp"
unfolding sameDom_def lift_def
by (auto simp: option.case_eq_if)  

lemma sameDom_lift_simp1[simp]:
"sameDom inp (lift f inp') = sameDom inp inp'"
unfolding sameDom_def lift_def by (force simp: fun_eq_iff option.case_eq_if) 

lemma sameDom_lift_simp2[simp]:
"sameDom (lift f inp) inp' = sameDom inp inp'"
unfolding sameDom_def lift_def by (force simp: fun_eq_iff option.case_eq_if)

lemma lift_preserves_sameDom:
assumes "sameDom inp inp'"
shows "sameDom (lift f inp) (lift g inp')"
using assms unfolding sameDom_def lift_def 
by (force simp: fun_eq_iff option.case_eq_if)
 
definition comp2 ::
"('b1 ⇒ 'b2 ⇒ 'c) ⇒ ('a1 ⇒ 'b1) ⇒ ('a2 ⇒ 'b2) ⇒ ('a1 ⇒ 'a2 ⇒ 'c)"
("_ o2 '(_,_')" 55)
where "h o2 (f,g) == λ x y. h (f x) (g y)"

lemma comp2_simp[simp]:
"(h o2 (f,g)) x y = h (f x) (g y)"
unfolding comp2_def by simp

lemma comp2_comp:
"((h o2 (f,g)) o2 (f',g')) = (h o2 (f o f', g o g'))"
unfolding comp_def[abs_def] comp2_def[abs_def] by auto

lemma liftAll_imp_liftAll2:
assumes "liftAll (λv. ∀ v'. phi v v') inp"
shows "liftAll2 phi inp inp'"
using assms unfolding liftAll_def liftAll2_def by auto

lemma liftAll2_mono:
assumes "⋀ v v'. phi v v' ⟹ chi v v'" and "liftAll2 phi inp inp'"
shows "liftAll2 chi inp inp'"
using assms unfolding liftAll2_def by blast

lemma liftAll2_True: "liftAll2 (λ v v'. True) inp inp'"
unfolding liftAll2_def by auto

lemma liftAll2_lift_comp2:
"liftAll2 phi (lift f1 inp1) (lift f2 inp2) =
 liftAll2 (phi o2 (f1,f2)) inp1 inp2"
unfolding liftAll2_def lift_def 
by (auto simp: fun_eq_iff option.case_eq_if)
 
lemma lift_imp_sameDom:
"lift f inp = lift f inp' ⟹ sameDom inp inp'"
unfolding lift_def sameDom_def
by (force simp: fun_eq_iff option.case_eq_if split: if_splits)
 
lemma lift_lift2:
"lift f (lift2 g inp' inp) =
 lift2 (λ v' v. f (g v' v)) inp' inp"
unfolding lift_def lift2_def 
by (force simp: option.case_eq_if split: if_splits) 

lemma lift2_left[simp]:
assumes "sameDom inp' inp"
shows "lift2 (λ v' v. v') inp' inp = inp'"
using assms unfolding sameDom_def lift2_def 
by (simp add: fun_eq_iff option.case_eq_if) metis
 
lemma lift2_right[simp]:
assumes "sameDom inp' inp"
shows "lift2 (λ v' v. v) inp' inp = inp"
using assms unfolding sameDom_def lift2_def 
by (simp add: fun_eq_iff option.case_eq_if)  

lemma lift2_preserves_sameDom:
assumes "sameDom inp' inp1'" and "sameDom inp inp1"
shows "sameDom (lift2 f inp' inp) (lift2 g inp1' inp1)"
using assms unfolding sameDom_def lift2_def 
by (simp add: fun_eq_iff option.case_eq_if)  

lemma sameDom_lift2_1:
assumes "sameDom inp' inp"
shows
"sameDom inp' (lift2 f inp' inp) ∧
 sameDom inp (lift2 f inp' inp)"
using assms unfolding sameDom_def lift2_def 
by (simp add: fun_eq_iff option.case_eq_if)  

lemma sameDom_lift2_2:
assumes "sameDom inp' inp"
shows
"sameDom (lift2 f inp' inp) inp' ∧
 sameDom (lift2 f inp' inp) inp"
using assms unfolding sameDom_def lift2_def 
by (simp add: fun_eq_iff option.case_eq_if)  

lemma sameDom_lift2_simp1[simp]:
assumes "sameDom inp1' inp1"
shows "sameDom inp (lift2 f inp1' inp1) = sameDom inp inp1'"
using assms unfolding sameDom_def lift2_def 
by (simp add: fun_eq_iff option.case_eq_if) (metis not_Some_eq)

lemma sameDom_lift2_simp2[simp]:
assumes "sameDom inp' inp"
shows "sameDom (lift2 f inp' inp) inp1 = sameDom inp' inp1"
using assms unfolding sameDom_def lift2_def 
by (simp add: fun_eq_iff option.case_eq_if) (metis not_Some_eq)

lemma liftAll2_lift_ext:
"(sameDom inp inp' ∧ liftAll2 (λ v v'. f v = f v') inp inp') =
 (lift f inp = lift f inp')"
unfolding sameDom_def lift_def liftAll2_def 
by (force simp add: fun_eq_iff option.case_eq_if) 

lemma liftAll2_and:
"liftAll2 (λ v v'. phi v v' ∧ chi v v') inp inp' =
(liftAll2 phi inp inp' ∧ liftAll2 chi inp inp')"
unfolding liftAll2_def by force

lemma liftAll2_mp:
assumes "liftAll2 (λ v v'. phi v v' ⟶ chi v v') inp inp'" and "liftAll2 phi inp inp'"
shows "liftAll2 chi inp inp'"
using assms unfolding liftAll2_def by auto

lemma sameDom_and_liftAll2_iff:
"(sameDom inp inp' ∧ liftAll2 phi inp inp') =
 (∀ i. (inp i = None ∧ inp' i = None) ∨
         (∃ v v'. inp i = Some v ∧ inp' i = Some v' ∧ phi v v'))"
unfolding sameDom_def liftAll2_def 
apply (auto simp add: fun_eq_iff option.case_eq_if) 
using option.sel by fastforce

subsection ‹Doubly infinitely-branching trees›

text "These simple infinitary trees shall be used for measuring the sizes
  of possibly infinitary terms."

datatype ('index,'bindex)tree =
  Branch "('index,('index,'bindex)tree) input" "('bindex,('index,'bindex)tree) input"


(* The natural induction principle for (infinitary) trees:  *)
lemma tree_induct:
fixes phi::"('index,'bindex)tree ⇒ bool" and T::"('index,'bindex)tree"
assumes
  "⋀ inp binp. ⟦liftAll phi inp; liftAll phi binp⟧ ⟹ phi (Branch inp binp)"
shows "phi T"
using assms unfolding liftAll_def  
by (induct T) (simp, metis rangeI) 

definition treeLess :: "('index,'bindex)tree rel"
where
"treeLess ==
 {(T,T'). ∃ inp binp i j. T' = Branch inp binp ∧ (inp i = Some T ∨ binp j = Some T)}"

lemma treeLess_induct:
fixes phi::"('index,'bindex)tree ⇒ bool" and
      T::"('index,'bindex)tree"
assumes "⋀ T'. (⋀ T. (T,T') ∈ treeLess ⟹ phi T) ⟹ phi T'"
shows "phi T"
apply(induct rule: tree_induct)
using assms unfolding treeLess_def liftAll_def  
by simp (metis tree.inject) 

lemma treeLess_wf: "wf treeLess"
unfolding wf_def using treeLess_induct by blast


subsection ‹Ordering›

lemma Least_Max:
assumes phi: "phi (n::nat)" and fin: "finite {n. phi n}"
shows "(LEAST m. ∀ n. phi n ⟶ n ≤ m) =
       Max {n. phi n}" 
using assms Max_in by (intro Least_equality) auto


end

section ‹Quasi-Terms with Swapping and Freshness›

theory QuasiTerms_Swap_Fresh imports Preliminaries 
begin

text‹
This section defines and studies the (totally free) datatype of quasi-terms
and the notions of freshness and
swapping variables for them.
``Quasi" refers to the fact that these items are not (yet) factored to alpha-equivalence.
 We shall later call ``terms" those alpha-equivalence classes.›

subsection ‹The datatype of quasi-terms with bindings›

datatype
('index,'bindex,'varSort,'var,'opSym)qTerm =
   qVar 'varSort 'var
  |qOp 'opSym "('index, (('index,'bindex,'varSort,'var,'opSym)qTerm))input"
              "('bindex, (('index,'bindex,'varSort,'var,'opSym)qAbs)) input"
and
('index,'bindex,'varSort,'var,'opSym)qAbs =
  qAbs 'varSort 'var "('index,'bindex,'varSort,'var,'opSym)qTerm"

text‹Above:
\begin{itemize}
\item ``Var" stands for ``variable injection"
\item ``Op" stands for ``operation"
\item ``opSym" stands for ``operation symbol"
\item ``q" stands for ``quasi"
\item ``Abs" stands for ``abstraction"
\end{itemize}

Thus, a quasi-term is either (an injection of) a variable, or an operation symbol applied
to a term-input and an abstraction-input
(where, for any type $T$, $T$-inputs are partial
maps from indexes to $T$. A quasi-abstraction is
essentially a pair (variable,quasi-term).
›

type_synonym ('index,'bindex,'varSort,'var,'opSym)qTermItem =
"('index,'bindex,'varSort,'var,'opSym)qTerm +
 ('index,'bindex,'varSort,'var,'opSym)qAbs"

abbreviation termIn ::
"('index,'bindex,'varSort,'var,'opSym)qTerm ⇒ ('index,'bindex,'varSort,'var,'opSym)qTermItem"
where "termIn X == Inl X"

abbreviation absIn ::
"('index,'bindex,'varSort,'var,'opSym)qAbs ⇒ ('index,'bindex,'varSort,'var,'opSym)qTermItem"
where "absIn A == Inr A"

subsection ‹Induction principles›

definition qTermLess :: "('index,'bindex,'varSort,'var,'opSym)qTermItem rel"
where
"qTermLess == {(termIn X, termIn(qOp delta inp binp))| X delta inp binp i. inp i = Some X} ∪
              {(absIn A, termIn(qOp delta inp binp))| A delta inp binp i. binp i = Some A} ∪
              {(termIn X, absIn (qAbs xs x X))| X xs x. True}"

text‹This induction will be used only temporarily, until we
   get a better one, involving swapping:›

lemma qTerm_rawInduct[case_names Var Op Abs]:
fixes X :: "('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A :: "('index,'bindex,'varSort,'var,'opSym)qAbs" and phi phiAbs
assumes
  Var: "⋀ xs x. phi (qVar xs x)" and
  Op: "⋀ delta inp binp. ⟦liftAll phi inp; liftAll phiAbs binp⟧ ⟹ phi (qOp delta inp binp)" and
  Abs: "⋀ xs x X. phi X ⟹ phiAbs (qAbs xs x X)"
shows "phi X ∧ phiAbs A"
by (induct rule: qTerm_qAbs.induct)
   (fastforce intro!: Var Op Abs rangeI simp: liftAll_def)+

lemma qTermLess_wf: "wf qTermLess" 
unfolding wf_def proof safe
  fix chi item
  assume *: "∀item. (∀item'. (item', item) ∈ qTermLess ⟶ chi item') ⟶ chi item"
  show "chi item"
  proof-
    {fix X A
     have "chi (termIn X) ∧ chi (absIn A)"
     apply(induct rule: qTerm_rawInduct)
     using * unfolding qTermLess_def liftAll_def by blast+
    }
    thus ?thesis by(cases item) auto
  qed
qed

lemma qTermLessPlus_wf: "wf (qTermLess ^+)"
using qTermLess_wf wf_trancl by auto

text‹The skeleton of a quasi-term item -- this is the generalization
   of the size function from the case of finitary syntax.
   We use the skeleton later for proving correct various recursive function definitions, notably that of ``alpha".›

function
qSkel :: "('index,'bindex,'varSort,'var,'opSym)qTerm ⇒ ('index,'bindex)tree"
and
qSkelAbs :: "('index,'bindex,'varSort,'var,'opSym)qAbs ⇒ ('index,'bindex)tree"
where
"qSkel (qVar xs x) = Branch (λi. None) (λi. None)"
|
"qSkel (qOp delta inp binp) = Branch (lift qSkel inp) (lift qSkelAbs binp)"
|
"qSkelAbs (qAbs xs x X) = Branch (λi. Some(qSkel X)) (λi. None)"
by(pat_completeness, auto)
termination by(relation qTermLess, simp add: qTermLess_wf, auto simp add: qTermLess_def)

text‹Next is a template for generating induction principles whenever we come up
  with relation on terms included in the kernel of the skeleton operator.›

lemma qTerm_templateInduct[case_names Var Op Abs]:
fixes X :: "('index,'bindex,'varSort,'var,'opSym)qTerm"
and A :: "('index,'bindex,'varSort,'var,'opSym)qAbs"
and phi phiAbs and rel
assumes
REL: "⋀ X Y. (X,Y) ∈ rel ⟹ qSkel Y = qSkel X" and
Var: "⋀ xs x. phi (qVar xs x)" and
Op: "⋀ delta inp binp. ⟦liftAll phi inp; liftAll phiAbs binp⟧
                       ⟹ phi (qOp delta inp binp)" and
Abs: "⋀ xs x X. (⋀ Y. (X,Y) ∈ rel ⟹ phi Y) ⟹ phiAbs (qAbs xs x X)"
shows "phi X ∧ phiAbs A" 
proof-
  {fix T
   have "∀ X A. (T = qSkel X ⟶ phi X) ∧ (T = qSkelAbs A ⟶ phiAbs A)"
   proof(induct rule: treeLess_induct)
     case (1 T')
     show ?case apply safe  
      subgoal for X _ 
      using assms 1 unfolding treeLess_def liftAll_def 
      by (cases X) (auto simp add: lift_def, metis option.simps(5))
     subgoal for _ A apply (cases A)
     using assms 1 unfolding treeLess_def by simp .       
   qed
  }
  thus ?thesis by blast
qed

text‹A modification of the canonical immediate-subterm
relation on quasi-terms, that takes into account a relation assumed included in the skeleton kernel.›

definition qTermLess_modulo ::
"('index,'bindex,'varSort,'var,'opSym)qTerm rel ⇒
 ('index,'bindex,'varSort,'var,'opSym)qTermItem rel"
where
"qTermLess_modulo rel ==
 {(termIn X, termIn(qOp delta inp binp))| X delta inp binp i. inp i = Some X} ∪
 {(absIn A, termIn(qOp delta inp binp))| A delta inp binp j. binp j = Some A} ∪
 {(termIn Y, absIn (qAbs xs x X))| X Y xs x. (X,Y) ∈ rel}"

lemma qTermLess_modulo_wf:
fixes rel::"('index,'bindex,'varSort,'var,'opSym)qTerm rel"
assumes "⋀ X Y. (X,Y) ∈ rel ⟹ qSkel Y = qSkel X"
shows "wf (qTermLess_modulo rel)"
proof(unfold wf_def, auto)
  fix chi item
  assume *:
  "∀item. (∀item'. (item', item) ∈ qTermLess_modulo rel  ⟶ chi item')
           ⟶ chi item"
  show "chi item"
  proof-
    obtain phi where phi_def: "phi = (λ X. chi (termIn X))" by blast
    obtain phiAbs where phiAbs_def: "phiAbs = (λ A. chi (absIn A))" by blast
    {fix X A
     have "chi (termIn X) ∧ chi (absIn A)"
     apply(induct rule: qTerm_templateInduct[of rel])
     using * assms unfolding qTermLess_modulo_def liftAll_def by blast+
    }
    thus ?thesis unfolding phi_def phiAbs_def
    by(cases item, auto)
  qed
qed

subsection ‹Swap and substitution on variables›

definition sw :: "'varSort ⇒ 'var ⇒ 'var ⇒ 'varSort ⇒ 'var ⇒ 'var"
where
"sw ys y1 y2 xs x ==
 if ys = xs then if x = y1 then y2
            else if x = y2 then y1
                           else x
 else x"

abbreviation sw_abbrev :: "'var ⇒ 'varSort ⇒ 'var ⇒ 'var ⇒ 'varSort ⇒ 'var"
("_ @_[_ ∧ _]'__" 200)
where "(x @xs[y1 ∧ y2]_ys) == sw ys y1 y2 xs x"

definition sb :: "'varSort ⇒ 'var ⇒ 'var ⇒ 'varSort ⇒ 'var ⇒ 'var"
where
"sb ys y1 y2 xs x ==
 if ys = xs then if x = y2 then y1
                           else x
 else x"

abbreviation sb_abbrev :: "'var ⇒ 'varSort ⇒ 'var ⇒ 'var ⇒ 'varSort ⇒ 'var"
("_ @_[_ '/ _]'__" 200)
where "(x @xs[y1 / y2]_ys) == sb ys y1 y2 xs x"

theorem sw_simps1[simp]: "(x @xs[x ∧ y]_xs) = y"
unfolding sw_def by simp

theorem sw_simps2[simp]: "(x @xs[y ∧ x]_xs) = y"
unfolding sw_def by simp

theorem sw_simps3[simp]:
"(zs ≠ xs ∨ x ∉ {z1,z2}) ⟹ (x @xs[z1 ∧ z2]_zs) = x"
unfolding sw_def by simp

lemmas sw_simps = sw_simps1 sw_simps2 sw_simps3

theorem sw_ident[simp]: "(x @xs[y ∧ y]_ys) = x"
unfolding sw_def by auto

theorem sw_compose:
"((z @zs[x ∧ y]_xs) @zs[x' ∧ y']_xs') =
 ((z @zs[x' ∧ y']_xs') @zs[(x @xs[x' ∧ y']_xs') ∧ (y @xs[x' ∧ y']_xs')]_xs)"
by(unfold sw_def, auto)

theorem sw_commute:
assumes "zs ≠ zs' ∨ {x,y} Int {x',y'} = {}"
shows "((u @us[x ∧ y]_zs) @us[x' ∧ y']_zs') = ((u @us[x' ∧ y']_zs') @us[x ∧ y]_zs)"
using assms by(unfold sw_def, auto)

theorem sw_involutive[simp]:
"((z @zs[x ∧ y]_xs) @zs[x ∧ y]_xs) = z"
by(unfold sw_def, auto)

theorem sw_inj[simp]:
"((z @zs[x ∧ y]_xs) = (z' @zs[x ∧ y]_xs)) = (z = z')"
by (simp add: sw_def) 

lemma sw_preserves_mship[simp]:
assumes "{y1,y2} ⊆ Var ys"
shows "((x @xs[y1 ∧ y2]_ys) ∈ Var xs) = (x ∈ Var xs)"
using assms unfolding sw_def by auto

theorem sw_sym:
"(z @zs[x ∧ y]_xs) = (z @zs[y ∧ x]_xs)"
by (unfold sw_def) auto

theorem sw_involutive2[simp]:
"((z @zs[x ∧ y]_xs) @zs[y ∧ x]_xs) = z"
by (unfold sw_def) auto

theorem sw_trans:
"us ≠ zs ∨ u ∉ {y,z} ⟹
 ((u @us[y ∧ x]_zs) @us[z ∧ y]_zs) = (u @us[z ∧ x]_zs)"
by (unfold sw_def) auto

lemmas sw_otherSimps =
sw_ident sw_involutive sw_inj sw_preserves_mship sw_involutive2

theorem sb_simps1[simp]: "(x @xs[y / x]_xs) = y"
unfolding sb_def by simp

theorem sb_simps2[simp]:
"(zs ≠ xs ∨ z2 ≠ x) ⟹ (x @xs[z1 / z2]_zs) = x"
unfolding sb_def by auto

lemmas sb_simps = sb_simps1 sb_simps2

theorem sb_ident[simp]: "(x @xs[y / y]_ys) = x"
unfolding sb_def by auto

theorem sb_compose1:
"((z @zs[y1 / x]_xs) @zs[y2 / x]_xs) = (z @zs[(y1 @xs[y2 / x]_xs) / x]_xs)"
by(unfold sb_def, auto)

theorem sb_compose2:
"ys ≠ xs ∨ (x2 ∉ {y1,y2}) ⟹
 ((z @zs[x1 / x2]_xs) @zs[y1 / y2]_ys) =
 ((z @zs[y1 / y2]_ys) @zs[(x1 @xs[y1 / y2]_ys) / x2]_xs)"
by (unfold sb_def) auto

theorem sb_commute:
assumes "zs ≠ zs' ∨ {x,y} Int {x',y'} = {}"
shows "((u @us[x / y]_zs) @us[x' / y']_zs') = ((u @us[x' / y']_zs') @us[x / y]_zs)"
using assms by (unfold sb_def) auto

theorem sb_idem[simp]:
"((z @zs[x / y]_xs) @zs[x / y]_xs) = (z @zs[x / y]_xs)"
by (unfold sb_def) auto

lemma sb_preserves_mship[simp]:
assumes "{y1,y2} ⊆ Var ys"
shows "((x @xs[y1 / y2]_ys) ∈ Var xs) = (x ∈ Var xs)"
using assms by (unfold sb_def) auto

theorem sb_trans:
"us ≠ zs ∨ u ≠ y ⟹
 ((u @us[y / x]_zs) @us[z / y]_zs) = (u @us[z / x]_zs)"
by (unfold sb_def) auto

lemmas sb_otherSimps =
sb_ident sb_idem sb_preserves_mship

subsection ‹The swapping and freshness operators›

text ‹For establishing the preliminary results quickly, we use both the notion of
binding-sensitive freshness (operator ``qFresh")
       and that of ``absolute" freshness, ignoring bindings (operator ``qAFresh").  Later,
       for alpha-equivalence classes, ``qAFresh" will not make sense.›

definition
aux_qSwap_ignoreFirst3 ::
"'varSort * 'var * 'var * ('index,'bindex,'varSort,'var,'opSym)qTerm +
 'varSort * 'var * 'var * ('index,'bindex,'varSort,'var,'opSym)qAbs ⇒
 ('index,'bindex,'varSort,'var,'opSym)qTermItem"
where
"aux_qSwap_ignoreFirst3 K =
 (case K of Inl(zs,x,y,X) ⇒ termIn X
           |Inr(zs,x,y,A) ⇒ absIn A)"

lemma qTermLess_ingoreFirst3_wf:
"wf(inv_image qTermLess aux_qSwap_ignoreFirst3)"
using qTermLess_wf wf_inv_image by auto

function
qSwap :: "'varSort ⇒ 'var ⇒ 'var ⇒ ('index,'bindex,'varSort,'var,'opSym)qTerm ⇒
          ('index,'bindex,'varSort,'var,'opSym)qTerm"
and
qSwapAbs :: "'varSort ⇒ 'var ⇒ 'var ⇒ ('index,'bindex,'varSort,'var,'opSym)qAbs ⇒
             ('index,'bindex,'varSort,'var,'opSym)qAbs"
where
"qSwap zs x y (qVar zs' z) = qVar zs' (z @zs'[x ∧ y]_zs)"
|
"qSwap zs x y (qOp delta inp binp) =
 qOp delta (lift (qSwap zs x y) inp) (lift (qSwapAbs zs x y) binp)"
|
"qSwapAbs zs x y (qAbs zs' z X) = qAbs zs' (z @zs'[x ∧ y]_zs) (qSwap zs x y X)"
by(pat_completeness, auto)
termination
by(relation "inv_image qTermLess aux_qSwap_ignoreFirst3",
   simp add: qTermLess_ingoreFirst3_wf,
   auto simp add: qTermLess_def aux_qSwap_ignoreFirst3_def)

lemmas qSwapAll_simps = qSwap.simps qSwapAbs.simps

abbreviation qSwap_abbrev ::
  "('index,'bindex,'varSort,'var,'opSym)qTerm ⇒ 'var ⇒ 'var ⇒ 'varSort ⇒
   ('index,'bindex,'varSort,'var,'opSym)qTerm" ("_ #[[_ ∧ _]]'__" 200)
where "(X #[[z1 ∧ z2]]_zs) == qSwap zs z1 z2 X"

abbreviation qSwapAbs_abbrev ::
  "('index,'bindex,'varSort,'var,'opSym)qAbs ⇒ 'var ⇒ 'var ⇒ 'varSort ⇒
   ('index,'bindex,'varSort,'var,'opSym)qAbs" ("_ $[[_ ∧ _]]'__" 200)
where "(A $[[z1 ∧ z2]]_zs) == qSwapAbs zs z1 z2 A"

definition
aux_qFresh_ignoreFirst2 ::
"'varSort * 'var * ('index,'bindex,'varSort,'var,'opSym)qTerm +
 'varSort * 'var * ('index,'bindex,'varSort,'var,'opSym)qAbs ⇒
 ('index,'bindex,'varSort,'var,'opSym)qTermItem"
where
"aux_qFresh_ignoreFirst2 K =
 (case K of Inl(zs,x,X) ⇒ termIn X
           |Inr (zs,x,A) ⇒ absIn A)"

lemma qTermLess_ingoreFirst2_wf: "wf(inv_image qTermLess aux_qFresh_ignoreFirst2)"
using qTermLess_wf wf_inv_image by auto

text‹The quasi absolutely-fresh predicate:
  (note that this is not an oxymoron: ``quasi" refers
   to being an operator on quasi-terms, and not on
terms, i.e., on alpha-equivalence  classes;
   ``absolutely'' refers to not ignoring bindings in the notion of freshness,
and thus counting absolutely all the variables.›

function
qAFresh :: "'varSort ⇒ 'var ⇒ ('index,'bindex,'varSort,'var,'opSym)qTerm ⇒ bool"
and
qAFreshAbs :: "'varSort ⇒ 'var ⇒ ('index,'bindex,'varSort,'var,'opSym)qAbs ⇒ bool"
where
"qAFresh xs x (qVar ys y) = (xs ≠ ys ∨ x ≠ y)"
|
"qAFresh xs x (qOp delta inp binp) =
 (liftAll (qAFresh xs x) inp ∧ liftAll (qAFreshAbs xs x) binp)"
|
"qAFreshAbs xs x (qAbs ys y X) = ((xs ≠ ys ∨ x ≠ y) ∧ qAFresh xs x X)"
by(pat_completeness, auto)
termination
by(relation "inv_image qTermLess aux_qFresh_ignoreFirst2",
   simp add: qTermLess_ingoreFirst2_wf,
   auto simp add: qTermLess_def aux_qFresh_ignoreFirst2_def)

lemmas qAFreshAll_simps = qAFresh.simps qAFreshAbs.simps

text‹The next is standard freshness -- note that its definition differs from that
of absolute freshness only at the clause for abstractions.›

function
qFresh :: "'varSort ⇒ 'var ⇒ ('index,'bindex,'varSort,'var,'opSym)qTerm ⇒ bool"
and
qFreshAbs :: "'varSort ⇒ 'var ⇒ ('index,'bindex,'varSort,'var,'opSym)qAbs ⇒ bool"
where
"qFresh xs x (qVar ys y) = (xs ≠ ys ∨ x ≠ y)"
|
"qFresh xs x (qOp delta inp binp) =
 (liftAll (qFresh xs x) inp ∧ liftAll (qFreshAbs xs x) binp)"
|
"qFreshAbs xs x (qAbs ys y X) = ((xs = ys ∧ x = y) ∨ qFresh xs x X)"
by(pat_completeness, auto)
termination
by(relation "inv_image qTermLess aux_qFresh_ignoreFirst2",
   simp add: qTermLess_ingoreFirst2_wf,
   auto simp add: qTermLess_def aux_qFresh_ignoreFirst2_def)

lemmas qFreshAll_simps = qFresh.simps qFreshAbs.simps

subsection ‹Compositional properties of swapping›

lemma qSwapAll_ident:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs"
    shows "(X #[[x ∧ x]]_zs) = X ∧ (A $[[x ∧ x]]_zs) = A"
  by (induct rule: qTerm_rawInduct)
     (auto simp add: liftAll_def lift_cong lift_ident)

corollary qSwap_ident[simp]: "(X #[[x ∧ x]]_zs) = X"
by(simp add: qSwapAll_ident)

lemma qSwapAll_compose:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm"  and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and zs x y x' y'
shows
"((X #[[x ∧ y]]_zs) #[[x' ∧ y']]_zs') =
 ((X #[[x' ∧ y']]_zs') #[[(x @zs[x' ∧ y']_zs') ∧ (y @zs[x' ∧ y']_zs')]]_zs)
∧
 ((A $[[x ∧ y]]_zs) $[[x' ∧ y']]_zs') =
 ((A $[[x' ∧ y']]_zs') $[[(x @zs[x' ∧ y']_zs') ∧ (y @zs[x' ∧ y']_zs')]]_zs)"
proof(induct rule: qTerm_rawInduct[of _ _ X A])
  case (Op delta inp binp)
  then show ?case by (auto intro!: lift_cong simp: liftAll_def lift_comp)
qed (auto simp add: sw_def sw_compose)
  
corollary qSwap_compose:
"((X #[[x ∧ y]]_zs) #[[x' ∧ y']]_zs') =
 ((X #[[x' ∧ y']]_zs') #[[(x @zs[x' ∧ y']_zs') ∧ (y @zs[x' ∧ y']_zs')]]_zs)"
by (meson qSwapAll_compose)

lemma qSwap_commute:
assumes "zs ≠ zs' ∨ {x,y} Int {x',y'} = {}"
shows "((X #[[x ∧ y]]_zs) #[[x' ∧ y']]_zs') = ((X #[[x' ∧ y']]_zs') #[[x ∧ y]]_zs)"
by (metis assms disjoint_insert(1) qSwapAll_compose sw_simps3)

lemma qSwapAll_involutive:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and zs x y
shows "((X #[[x ∧ y]]_zs) #[[x ∧ y]]_zs) = X ∧
       ((A $[[x ∧ y]]_zs) $[[x ∧ y]]_zs) = A"
proof(induct rule: qTerm_rawInduct[of _ _ X A])
  case (Op delta inp binp)
  then show ?case 
    unfolding qSwapAll_simps(2) liftAll_lift_ext
    lift_comp o_def
    by (simp add: lift_ident)
qed(auto)
  

corollary qSwap_involutive[simp]:
"((X #[[x ∧ y]]_zs) #[[x ∧ y]]_zs) = X"
by(simp add: qSwapAll_involutive)

lemma qSwapAll_sym:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and zs x y
shows "(X #[[x ∧ y]]_zs) = (X #[[y ∧ x]]_zs) ∧
       (A $[[x ∧ y]]_zs) = (A $[[y ∧ x]]_zs)"
by (induct rule: qTerm_rawInduct[of _ _ X A])  
   (auto simp: sw_sym lift_comp liftAll_lift_ext)

corollary qSwap_sym:
"(X #[[x ∧ y]]_zs) = (X #[[y ∧ x]]_zs)"
by(simp add: qSwapAll_sym)

lemma qAFreshAll_qSwapAll_id:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and zs z1 z2
shows "(qAFresh zs z1 X ∧ qAFresh zs z2 X  ⟶ (X #[[z1 ∧ z2]]_zs) = X) ∧
       (qAFreshAbs zs z1 A ∧ qAFreshAbs zs z2 A  ⟶ (A $[[z1 ∧ z2]]_zs) = A)"
by (induct rule: qTerm_rawInduct[of _ _ X A])
   (auto intro!: ext simp: liftAll_def lift_def option.case_eq_if)

corollary qAFresh_qSwap_id[simp]:
"⟦qAFresh zs z1 X; qAFresh zs z2 X⟧  ⟹ (X #[[z1 ∧ z2]]_zs) = X"
by(simp add: qAFreshAll_qSwapAll_id)

lemma qAFreshAll_qSwapAll_compose:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs"and zs x y z
shows  "(qAFresh zs y X ∧ qAFresh zs z X ⟶
         ((X #[[y ∧ x]]_zs) #[[z ∧ y]]_zs) = (X #[[z ∧ x]]_zs)) ∧
        (qAFreshAbs zs y A ∧ qAFreshAbs zs z A ⟶
         ((A $[[y ∧ x]]_zs) $[[z ∧ y]]_zs) = (A $[[z ∧ x]]_zs))"
by (induct rule: qTerm_rawInduct[of _ _ X A])
   (auto intro!: ext simp: sw_trans lift_comp lift_def liftAll_def option.case_eq_if)
   
corollary qAFresh_qSwap_compose:
"⟦qAFresh zs y X; qAFresh zs z X⟧ ⟹
 ((X #[[y ∧ x]]_zs) #[[z ∧ y]]_zs) = (X #[[z ∧ x]]_zs)"
by(simp add: qAFreshAll_qSwapAll_compose)

subsection ‹Induction and well-foundedness modulo swapping›

lemma qSkel_qSwapAll:
fixes  X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
       A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and x y zs
shows "qSkel(X #[[x ∧ y]]_zs) = qSkel X ∧
       qSkelAbs(A $[[x ∧ y]]_zs) = qSkelAbs A"
proof(induct rule: qTerm_rawInduct[of _ _ X A])
  case (Op delta inp binp)
  then show ?case 
    unfolding qSwapAll_simps(2) liftAll_lift_ext qSkel.simps(2)
    lift_comp comp_apply by simp
qed auto

corollary qSkel_qSwap: "qSkel(X #[[x ∧ y]]_zs) = qSkel X"
by(simp add: qSkel_qSwapAll)

text‹
  For induction modulo swapping, one may wish to swap not just once,
   but several times at the
   induction hypothesis (an example of this will be the proof of compatibility
   of ``qSwap" with alpha) -- for this, we introduce the following relation
  (the suffix ``Raw" signifies the fact that the involved variables are
  not required to be well-sorted):›

inductive_set qSwapped :: "('index,'bindex,'varSort,'var,'opSym)qTerm rel"
where
Refl: "(X,X) ∈ qSwapped"
|
Trans: "⟦(X,Y) ∈ qSwapped; (Y,Z) ∈ qSwapped⟧ ⟹ (X,Z) ∈ qSwapped"
|
Swap: "(X,Y) ∈ qSwapped ⟹ (X, Y #[[x ∧ y]]_zs) ∈ qSwapped"

lemmas qSwapped_Clauses = qSwapped.Refl qSwapped.Trans qSwapped.Swap

lemma qSwap_qSwapped: "(X, X #[[x ∧ y]]_zs): qSwapped"
by (auto simp add: qSwapped_Clauses)

lemma qSwapped_qSkel:
"(X,Y) ∈ qSwapped  ⟹ qSkel Y = qSkel X"
by(erule qSwapped.induct, auto simp add: qSkel_qSwap)

text‹The following is henceforth our main induction principle for quasi-terms.  At the
 clause for abstractions, the user may choose among the two
 induction hypotheses (IHs):
 \\-(1) IH for all swapped terms
 \\-(2) IH for all terms with the same skeleton.

The user may choose only one of the above, and ignore the others, but may of course also
assume both.  (2) is stronger than (1),
but we offer both of them for convenience in proofs.
Most of the times, (1) will be the most convenient.›

lemma qTerm_induct[case_names Var Op Abs]:
fixes X :: "('index,'bindex,'varSort,'var,'opSym)qTerm"
and A :: "('index,'bindex,'varSort,'var,'opSym)qAbs"  and phi phiAbs
assumes
  Var: "⋀ xs x. phi (qVar xs x)" and
  Op: "⋀ delta inp binp. ⟦liftAll phi inp; liftAll phiAbs binp⟧
                         ⟹ phi (qOp delta inp binp)" and
  Abs: "⋀ xs x X. ⟦⋀ Y. (X,Y) ∈ qSwapped ⟹ phi Y;
                    ⋀ Y. qSkel Y = qSkel X ⟹ phi Y⟧
                    ⟹ phiAbs (qAbs xs x X)"
shows "phi X ∧ phiAbs A"
  by (induct rule: qTerm_templateInduct[of "qSwapped ∪ {(X,Y). qSkel Y = qSkel X}"], 
      auto simp add: qSwapped_qSkel assms)


text‹The following relation will be needed for proving alpha-equivalence well-defined:›

definition qTermQSwappedLess :: "('index,'bindex,'varSort,'var,'opSym)qTermItem rel"
where "qTermQSwappedLess = qTermLess_modulo qSwapped"

lemma qTermQSwappedLess_wf: "wf qTermQSwappedLess"
unfolding qTermQSwappedLess_def
using qSwapped_qSkel qTermLess_modulo_wf[of qSwapped] by blast


subsection‹More properties connecting swapping and freshness›

lemma qSwap_3commute:
assumes *: "qAFresh ys y X" and **: "qAFresh ys y0 X"
and ***: "ys ≠ zs ∨ y0 ∉ {z1,z2}"
shows "((X #[[z1 ∧ z2]]_zs) #[[y0 ∧ x @ys[z1 ∧ z2]_zs]]_ys) =
       (((X #[[y ∧ x]]_ys) #[[y0 ∧ y]]_ys) #[[z1 ∧ z2]]_zs)"
proof-
  have "y0 = (y0 @ys[z1 ∧ z2]_zs)" using *** unfolding sw_def by auto
  hence "((X #[[z1 ∧ z2]]_zs) #[[y0 ∧ x @ys[z1 ∧ z2]_zs]]_ys) =
         ((X #[[y0 ∧ x]]_ys) #[[z1 ∧ z2]]_zs)"
  by(simp add: qSwap_compose[of _ z1])
  also have "((X #[[y0 ∧ x]]_ys) #[[z1 ∧ z2]]_zs) =
             (((X #[[y ∧ x]]_ys) #[[y0 ∧ y]]_ys) #[[z1 ∧ z2]]_zs)"
  using * ** by (simp add: qAFresh_qSwap_compose)
  finally show ?thesis .
qed

lemma qAFreshAll_imp_qFreshAll:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and xs x
shows "(qAFresh xs x X ⟶ qFresh xs x X) ∧
       (qAFreshAbs xs x A ⟶ qFreshAbs xs x A)"
by(induct rule: qTerm_rawInduct, auto simp add: liftAll_def)

corollary qAFresh_imp_qFresh:
"qAFresh xs x X ⟹ qFresh xs x X"
by(simp add: qAFreshAll_imp_qFreshAll)

lemma qSwapAll_preserves_qAFreshAll:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and ys y zs z1 z2
shows
"(qAFresh ys (y @ys[z1 ∧ z2]_zs) (X #[[z1 ∧ z2]]_zs) = qAFresh ys y X) ∧
 (qAFreshAbs ys (y @ys[z1 ∧ z2]_zs) (A $[[z1 ∧ z2]]_zs) = qAFreshAbs ys y A)"
proof(induct rule: qTerm_rawInduct[of _ _ X A])
  case (Op delta inp binp)
  then show ?case 
    unfolding qAFreshAll_simps(2) qSwapAll_simps(2) liftAll_lift_comp o_def 
    unfolding liftAll_def by presburger
qed(auto simp add: sw_def)

corollary qSwap_preserves_qAFresh[simp]:
"(qAFresh ys (y @ys[z1 ∧ z2]_zs) (X #[[z1 ∧ z2]]_zs) = qAFresh ys y X)"
by(simp add: qSwapAll_preserves_qAFreshAll)

lemma qSwap_preserves_qAFresh_distinct:
assumes "ys ≠ zs ∨ y ∉ {z1,z2}"
shows "qAFresh ys y (X #[[z1 ∧ z2]]_zs) = qAFresh ys y X"
proof-
  have "y = (y @ys[z1 ∧ z2]_zs)" using assms unfolding sw_def by auto
  thus ?thesis using qSwap_preserves_qAFresh[of ys zs z1 z2 y] by auto
qed

lemma qAFresh_qSwap_exchange1:
"qAFresh zs z2 (X #[[z1 ∧ z2]]_zs) = qAFresh zs z1 X"
proof-
  have "z2 = (z1 @zs[z1 ∧ z2]_zs)" unfolding sw_def by auto
  thus ?thesis using qSwap_preserves_qAFresh[of zs zs z1 z2 z1 X] by auto
qed

lemma qAFresh_qSwap_exchange2:
"qAFresh zs z2 (X #[[z2 ∧ z1]]_zs) = qAFresh zs z1 X"
by(auto simp add: qAFresh_qSwap_exchange1 qSwap_sym)

lemma qSwapAll_preserves_qFreshAll:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and ys y zs z1 z2
shows
"(qFresh ys (y @ys[z1 ∧ z2]_zs) (X #[[z1 ∧ z2]]_zs) = qFresh ys y X) ∧
 (qFreshAbs ys (y @ys[z1 ∧ z2]_zs) (A $[[z1 ∧ z2]]_zs) = qFreshAbs ys y A)"
proof(induct rule: qTerm_rawInduct[of _ _ X A])
  case (Op delta inp binp)
  then show ?case 
   unfolding qFreshAll_simps(2) qSwapAll_simps(2) liftAll_lift_comp o_def 
   unfolding liftAll_def by presburger
qed (auto simp add: sw_def)

corollary qSwap_preserves_qFresh:
"(qFresh ys (y @ys[z1 ∧ z2]_zs) (X #[[z1 ∧ z2]]_zs) = qFresh ys y X)"
by(simp add: qSwapAll_preserves_qFreshAll)

lemma qSwap_preserves_qFresh_distinct:
assumes "ys ≠ zs ∨ y ∉ {z1,z2}"
shows "qFresh ys y (X #[[z1 ∧ z2]]_zs) = qFresh ys y X"
proof-
  have "y = (y @ys[z1 ∧ z2]_zs)" using assms unfolding sw_def by auto
  thus ?thesis using qSwap_preserves_qFresh[of ys zs z1 z2 y] by auto
qed

lemma qFresh_qSwap_exchange1:
"qFresh zs z2 (X #[[z1 ∧ z2]]_zs) = qFresh zs z1 X"
proof-
  have "z2 = (z1 @zs[z1 ∧ z2]_zs)" unfolding sw_def by auto
  thus ?thesis using qSwap_preserves_qFresh[of zs zs z1 z2 z1 X] by auto
qed

lemma qFresh_qSwap_exchange2:
"qFresh zs z1 X = qFresh zs z2 (X #[[z2 ∧ z1]]_zs)"
by (auto simp add: qFresh_qSwap_exchange1 qSwap_sym)

lemmas qSwap_qAFresh_otherSimps =
qSwap_ident qSwap_involutive qAFresh_qSwap_id qSwap_preserves_qAFresh

end